a, b, c:. ((a + b) * (c + b)) = (((a * c) + (b * c)) + (b * b) + (a * b))   

latex

Definitions	P  Q, T, P & Q, P  Q, P  Q, True, t  T, x:A. B(x),
Lemmas	qadd comm q, qadd ac 1 q, mon assoc q, true wf, squash wf, qmul over plus qrng, qmul wf, qadd wf, rationals wf